/*
 * ConflictAnalyzerGenericTester.cuh
 *
 *  Created on: Oct 17, 2013
 *      Author: jaime
 */

#ifndef CONFLICTANALYZERGENERICTESTER_CUH_
#define CONFLICTANALYZERGENERICTESTER_CUH_

#include "../../ConflictAnalysis/ConflictAnalyzer.cuh"
#include "../../ConflictAnalysis/ConflictAnalyzerFullSearchSpace.cuh"
#include "../../ConflictAnalysis/ConflictAnalyzerWithWatchedLits.cuh"
#include "../../SATSolver/DataToDevice.cuh"
#include "../Tester.cuh"
#include "../../SATSolver/VariablesStateHandler.cuh"
#include "PropagationTester.cuh"

class ConflictAnalyzerGenericTester : public Tester {
private:
	ConflictAnalyzer conflictAnalyzer;
	ConflictAnalyzerFullSearchSpace conflictAnalyzer_fullsearch;
	ConflictAnalyzerWithWatchedLits conflictAnalyzer_two_literals;
	VariablesStateHandler * vars_handler;
	CUDAClauseVec * formula;
	int number_of_variables;
	int number_of_clauses;

#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
	GPUVec<Lit> assumptions(0);
#else
	GPUStaticVec<Lit, 16> assumptions;
#endif

public:
	__device__ ConflictAnalyzerGenericTester(DataToDevice & data,
			VariablesStateHandler * handler);

	__device__ bool test_init_states();
	__device__ bool test_resets();
	__device__ void test_all();
	__device__ bool test_propagates();
private:
	__device__ bool test_init_state(ConflictAnalyzer* analyzer);
	__device__ bool test_reset(ConflictAnalyzer* analyzer);
	__device__ bool test_propagate(ConflictAnalyzer* analyzer);
	__device__ bool perform_tests(
			bool (ConflictAnalyzerGenericTester::*funct_ptr)(ConflictAnalyzer* analyzer));
	__device__ bool change_analyzers_states();
};

#endif /* CONFLICTANALYZERGENERICTESTER_CUH_ */
